Left Termination of the query pattern s2(b,f) w.r.t. the given Prolog program could not be shown:



↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof

s22(plus2(A, plus2(B, C)), D) :- s22(plus2(plus2(A, B), C), D).
s22(plus2(A, B), C) :- s22(plus2(B, A), C).
s22(plus2(X, 00), X).
s22(plus2(X, Y), Z) :- s22(X, A), s22(Y, B), s22(plus2(A, B), Z).
s22(plus2(A, B), C) :- isNat1(A), isNat1(B), add3(A, B, C).
isNat1(s1(X)) :- isNat1(X).
isNat1(00).
add3(s1(X), Y, s1(Z)) :- add3(X, Y, Z).
add3(00, X, X).


With regard to the inferred argument filtering the predicates were used in the following modes:
s22: (b,f)
isNat1: (b)
add3: (b,b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:


s2_2_in_ga2(plus_22(A, plus_22(B, C)), D) -> if_s2_2_in_1_ga5(A, B, C, D, s2_2_in_ga2(plus_22(plus_22(A, B), C), D))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_2_ga4(A, B, C, s2_2_in_ga2(plus_22(B, A), C))
s2_2_in_ga2(plus_22(X, 0_0), X) -> s2_2_out_ga2(plus_22(X, 0_0), X)
s2_2_in_ga2(plus_22(X, Y), Z) -> if_s2_2_in_3_ga4(X, Y, Z, s2_2_in_ga2(X, A))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_6_ga4(A, B, C, isNat_1_in_g1(A))
isNat_1_in_g1(s_11(X)) -> if_isNat_1_in_1_g2(X, isNat_1_in_g1(X))
isNat_1_in_g1(0_0) -> isNat_1_out_g1(0_0)
if_isNat_1_in_1_g2(X, isNat_1_out_g1(X)) -> isNat_1_out_g1(s_11(X))
if_s2_2_in_6_ga4(A, B, C, isNat_1_out_g1(A)) -> if_s2_2_in_7_ga4(A, B, C, isNat_1_in_g1(B))
if_s2_2_in_7_ga4(A, B, C, isNat_1_out_g1(B)) -> if_s2_2_in_8_ga4(A, B, C, add_3_in_gga3(A, B, C))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_s2_2_in_8_ga4(A, B, C, add_3_out_gga3(A, B, C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_3_ga4(X, Y, Z, s2_2_out_ga2(X, A)) -> if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_in_ga2(Y, B))
if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_out_ga2(Y, B)) -> if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_in_ga2(plus_22(A, B), Z))
if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_out_ga2(plus_22(A, B), Z)) -> s2_2_out_ga2(plus_22(X, Y), Z)
if_s2_2_in_2_ga4(A, B, C, s2_2_out_ga2(plus_22(B, A), C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_1_ga5(A, B, C, D, s2_2_out_ga2(plus_22(plus_22(A, B), C), D)) -> s2_2_out_ga2(plus_22(A, plus_22(B, C)), D)

The argument filtering Pi contains the following mapping:
s2_2_in_ga2(x1, x2)  =  s2_2_in_ga1(x1)
plus_22(x1, x2)  =  plus_22(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
if_s2_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_1_ga1(x5)
if_s2_2_in_2_ga4(x1, x2, x3, x4)  =  if_s2_2_in_2_ga1(x4)
s2_2_out_ga2(x1, x2)  =  s2_2_out_ga1(x2)
if_s2_2_in_3_ga4(x1, x2, x3, x4)  =  if_s2_2_in_3_ga2(x2, x4)
if_s2_2_in_6_ga4(x1, x2, x3, x4)  =  if_s2_2_in_6_ga3(x1, x2, x4)
isNat_1_in_g1(x1)  =  isNat_1_in_g1(x1)
if_isNat_1_in_1_g2(x1, x2)  =  if_isNat_1_in_1_g1(x2)
isNat_1_out_g1(x1)  =  isNat_1_out_g
if_s2_2_in_7_ga4(x1, x2, x3, x4)  =  if_s2_2_in_7_ga3(x1, x2, x4)
if_s2_2_in_8_ga4(x1, x2, x3, x4)  =  if_s2_2_in_8_ga1(x4)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_s2_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_4_ga2(x4, x5)
if_s2_2_in_5_ga6(x1, x2, x3, x4, x5, x6)  =  if_s2_2_in_5_ga1(x6)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
  ↳ PrologToPiTRSProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

s2_2_in_ga2(plus_22(A, plus_22(B, C)), D) -> if_s2_2_in_1_ga5(A, B, C, D, s2_2_in_ga2(plus_22(plus_22(A, B), C), D))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_2_ga4(A, B, C, s2_2_in_ga2(plus_22(B, A), C))
s2_2_in_ga2(plus_22(X, 0_0), X) -> s2_2_out_ga2(plus_22(X, 0_0), X)
s2_2_in_ga2(plus_22(X, Y), Z) -> if_s2_2_in_3_ga4(X, Y, Z, s2_2_in_ga2(X, A))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_6_ga4(A, B, C, isNat_1_in_g1(A))
isNat_1_in_g1(s_11(X)) -> if_isNat_1_in_1_g2(X, isNat_1_in_g1(X))
isNat_1_in_g1(0_0) -> isNat_1_out_g1(0_0)
if_isNat_1_in_1_g2(X, isNat_1_out_g1(X)) -> isNat_1_out_g1(s_11(X))
if_s2_2_in_6_ga4(A, B, C, isNat_1_out_g1(A)) -> if_s2_2_in_7_ga4(A, B, C, isNat_1_in_g1(B))
if_s2_2_in_7_ga4(A, B, C, isNat_1_out_g1(B)) -> if_s2_2_in_8_ga4(A, B, C, add_3_in_gga3(A, B, C))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_s2_2_in_8_ga4(A, B, C, add_3_out_gga3(A, B, C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_3_ga4(X, Y, Z, s2_2_out_ga2(X, A)) -> if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_in_ga2(Y, B))
if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_out_ga2(Y, B)) -> if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_in_ga2(plus_22(A, B), Z))
if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_out_ga2(plus_22(A, B), Z)) -> s2_2_out_ga2(plus_22(X, Y), Z)
if_s2_2_in_2_ga4(A, B, C, s2_2_out_ga2(plus_22(B, A), C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_1_ga5(A, B, C, D, s2_2_out_ga2(plus_22(plus_22(A, B), C), D)) -> s2_2_out_ga2(plus_22(A, plus_22(B, C)), D)

The argument filtering Pi contains the following mapping:
s2_2_in_ga2(x1, x2)  =  s2_2_in_ga1(x1)
plus_22(x1, x2)  =  plus_22(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
if_s2_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_1_ga1(x5)
if_s2_2_in_2_ga4(x1, x2, x3, x4)  =  if_s2_2_in_2_ga1(x4)
s2_2_out_ga2(x1, x2)  =  s2_2_out_ga1(x2)
if_s2_2_in_3_ga4(x1, x2, x3, x4)  =  if_s2_2_in_3_ga2(x2, x4)
if_s2_2_in_6_ga4(x1, x2, x3, x4)  =  if_s2_2_in_6_ga3(x1, x2, x4)
isNat_1_in_g1(x1)  =  isNat_1_in_g1(x1)
if_isNat_1_in_1_g2(x1, x2)  =  if_isNat_1_in_1_g1(x2)
isNat_1_out_g1(x1)  =  isNat_1_out_g
if_s2_2_in_7_ga4(x1, x2, x3, x4)  =  if_s2_2_in_7_ga3(x1, x2, x4)
if_s2_2_in_8_ga4(x1, x2, x3, x4)  =  if_s2_2_in_8_ga1(x4)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_s2_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_4_ga2(x4, x5)
if_s2_2_in_5_ga6(x1, x2, x3, x4, x5, x6)  =  if_s2_2_in_5_ga1(x6)


Pi DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA2(plus_22(A, plus_22(B, C)), D) -> IF_S2_2_IN_1_GA5(A, B, C, D, s2_2_in_ga2(plus_22(plus_22(A, B), C), D))
S2_2_IN_GA2(plus_22(A, plus_22(B, C)), D) -> S2_2_IN_GA2(plus_22(plus_22(A, B), C), D)
S2_2_IN_GA2(plus_22(A, B), C) -> IF_S2_2_IN_2_GA4(A, B, C, s2_2_in_ga2(plus_22(B, A), C))
S2_2_IN_GA2(plus_22(A, B), C) -> S2_2_IN_GA2(plus_22(B, A), C)
S2_2_IN_GA2(plus_22(X, Y), Z) -> IF_S2_2_IN_3_GA4(X, Y, Z, s2_2_in_ga2(X, A))
S2_2_IN_GA2(plus_22(X, Y), Z) -> S2_2_IN_GA2(X, A)
S2_2_IN_GA2(plus_22(A, B), C) -> IF_S2_2_IN_6_GA4(A, B, C, isNat_1_in_g1(A))
S2_2_IN_GA2(plus_22(A, B), C) -> ISNAT_1_IN_G1(A)
ISNAT_1_IN_G1(s_11(X)) -> IF_ISNAT_1_IN_1_G2(X, isNat_1_in_g1(X))
ISNAT_1_IN_G1(s_11(X)) -> ISNAT_1_IN_G1(X)
IF_S2_2_IN_6_GA4(A, B, C, isNat_1_out_g1(A)) -> IF_S2_2_IN_7_GA4(A, B, C, isNat_1_in_g1(B))
IF_S2_2_IN_6_GA4(A, B, C, isNat_1_out_g1(A)) -> ISNAT_1_IN_G1(B)
IF_S2_2_IN_7_GA4(A, B, C, isNat_1_out_g1(B)) -> IF_S2_2_IN_8_GA4(A, B, C, add_3_in_gga3(A, B, C))
IF_S2_2_IN_7_GA4(A, B, C, isNat_1_out_g1(B)) -> ADD_3_IN_GGA3(A, B, C)
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> IF_ADD_3_IN_1_GGA4(X, Y, Z, add_3_in_gga3(X, Y, Z))
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> ADD_3_IN_GGA3(X, Y, Z)
IF_S2_2_IN_3_GA4(X, Y, Z, s2_2_out_ga2(X, A)) -> IF_S2_2_IN_4_GA5(X, Y, Z, A, s2_2_in_ga2(Y, B))
IF_S2_2_IN_3_GA4(X, Y, Z, s2_2_out_ga2(X, A)) -> S2_2_IN_GA2(Y, B)
IF_S2_2_IN_4_GA5(X, Y, Z, A, s2_2_out_ga2(Y, B)) -> IF_S2_2_IN_5_GA6(X, Y, Z, A, B, s2_2_in_ga2(plus_22(A, B), Z))
IF_S2_2_IN_4_GA5(X, Y, Z, A, s2_2_out_ga2(Y, B)) -> S2_2_IN_GA2(plus_22(A, B), Z)

The TRS R consists of the following rules:

s2_2_in_ga2(plus_22(A, plus_22(B, C)), D) -> if_s2_2_in_1_ga5(A, B, C, D, s2_2_in_ga2(plus_22(plus_22(A, B), C), D))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_2_ga4(A, B, C, s2_2_in_ga2(plus_22(B, A), C))
s2_2_in_ga2(plus_22(X, 0_0), X) -> s2_2_out_ga2(plus_22(X, 0_0), X)
s2_2_in_ga2(plus_22(X, Y), Z) -> if_s2_2_in_3_ga4(X, Y, Z, s2_2_in_ga2(X, A))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_6_ga4(A, B, C, isNat_1_in_g1(A))
isNat_1_in_g1(s_11(X)) -> if_isNat_1_in_1_g2(X, isNat_1_in_g1(X))
isNat_1_in_g1(0_0) -> isNat_1_out_g1(0_0)
if_isNat_1_in_1_g2(X, isNat_1_out_g1(X)) -> isNat_1_out_g1(s_11(X))
if_s2_2_in_6_ga4(A, B, C, isNat_1_out_g1(A)) -> if_s2_2_in_7_ga4(A, B, C, isNat_1_in_g1(B))
if_s2_2_in_7_ga4(A, B, C, isNat_1_out_g1(B)) -> if_s2_2_in_8_ga4(A, B, C, add_3_in_gga3(A, B, C))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_s2_2_in_8_ga4(A, B, C, add_3_out_gga3(A, B, C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_3_ga4(X, Y, Z, s2_2_out_ga2(X, A)) -> if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_in_ga2(Y, B))
if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_out_ga2(Y, B)) -> if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_in_ga2(plus_22(A, B), Z))
if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_out_ga2(plus_22(A, B), Z)) -> s2_2_out_ga2(plus_22(X, Y), Z)
if_s2_2_in_2_ga4(A, B, C, s2_2_out_ga2(plus_22(B, A), C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_1_ga5(A, B, C, D, s2_2_out_ga2(plus_22(plus_22(A, B), C), D)) -> s2_2_out_ga2(plus_22(A, plus_22(B, C)), D)

The argument filtering Pi contains the following mapping:
s2_2_in_ga2(x1, x2)  =  s2_2_in_ga1(x1)
plus_22(x1, x2)  =  plus_22(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
if_s2_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_1_ga1(x5)
if_s2_2_in_2_ga4(x1, x2, x3, x4)  =  if_s2_2_in_2_ga1(x4)
s2_2_out_ga2(x1, x2)  =  s2_2_out_ga1(x2)
if_s2_2_in_3_ga4(x1, x2, x3, x4)  =  if_s2_2_in_3_ga2(x2, x4)
if_s2_2_in_6_ga4(x1, x2, x3, x4)  =  if_s2_2_in_6_ga3(x1, x2, x4)
isNat_1_in_g1(x1)  =  isNat_1_in_g1(x1)
if_isNat_1_in_1_g2(x1, x2)  =  if_isNat_1_in_1_g1(x2)
isNat_1_out_g1(x1)  =  isNat_1_out_g
if_s2_2_in_7_ga4(x1, x2, x3, x4)  =  if_s2_2_in_7_ga3(x1, x2, x4)
if_s2_2_in_8_ga4(x1, x2, x3, x4)  =  if_s2_2_in_8_ga1(x4)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_s2_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_4_ga2(x4, x5)
if_s2_2_in_5_ga6(x1, x2, x3, x4, x5, x6)  =  if_s2_2_in_5_ga1(x6)
IF_S2_2_IN_3_GA4(x1, x2, x3, x4)  =  IF_S2_2_IN_3_GA2(x2, x4)
IF_S2_2_IN_6_GA4(x1, x2, x3, x4)  =  IF_S2_2_IN_6_GA3(x1, x2, x4)
ADD_3_IN_GGA3(x1, x2, x3)  =  ADD_3_IN_GGA2(x1, x2)
S2_2_IN_GA2(x1, x2)  =  S2_2_IN_GA1(x1)
IF_S2_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_S2_2_IN_1_GA1(x5)
IF_S2_2_IN_8_GA4(x1, x2, x3, x4)  =  IF_S2_2_IN_8_GA1(x4)
IF_S2_2_IN_2_GA4(x1, x2, x3, x4)  =  IF_S2_2_IN_2_GA1(x4)
IF_S2_2_IN_5_GA6(x1, x2, x3, x4, x5, x6)  =  IF_S2_2_IN_5_GA1(x6)
IF_ADD_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_ADD_3_IN_1_GGA1(x4)
ISNAT_1_IN_G1(x1)  =  ISNAT_1_IN_G1(x1)
IF_ISNAT_1_IN_1_G2(x1, x2)  =  IF_ISNAT_1_IN_1_G1(x2)
IF_S2_2_IN_7_GA4(x1, x2, x3, x4)  =  IF_S2_2_IN_7_GA3(x1, x2, x4)
IF_S2_2_IN_4_GA5(x1, x2, x3, x4, x5)  =  IF_S2_2_IN_4_GA2(x4, x5)

We have to consider all (P,R,Pi)-chains

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA2(plus_22(A, plus_22(B, C)), D) -> IF_S2_2_IN_1_GA5(A, B, C, D, s2_2_in_ga2(plus_22(plus_22(A, B), C), D))
S2_2_IN_GA2(plus_22(A, plus_22(B, C)), D) -> S2_2_IN_GA2(plus_22(plus_22(A, B), C), D)
S2_2_IN_GA2(plus_22(A, B), C) -> IF_S2_2_IN_2_GA4(A, B, C, s2_2_in_ga2(plus_22(B, A), C))
S2_2_IN_GA2(plus_22(A, B), C) -> S2_2_IN_GA2(plus_22(B, A), C)
S2_2_IN_GA2(plus_22(X, Y), Z) -> IF_S2_2_IN_3_GA4(X, Y, Z, s2_2_in_ga2(X, A))
S2_2_IN_GA2(plus_22(X, Y), Z) -> S2_2_IN_GA2(X, A)
S2_2_IN_GA2(plus_22(A, B), C) -> IF_S2_2_IN_6_GA4(A, B, C, isNat_1_in_g1(A))
S2_2_IN_GA2(plus_22(A, B), C) -> ISNAT_1_IN_G1(A)
ISNAT_1_IN_G1(s_11(X)) -> IF_ISNAT_1_IN_1_G2(X, isNat_1_in_g1(X))
ISNAT_1_IN_G1(s_11(X)) -> ISNAT_1_IN_G1(X)
IF_S2_2_IN_6_GA4(A, B, C, isNat_1_out_g1(A)) -> IF_S2_2_IN_7_GA4(A, B, C, isNat_1_in_g1(B))
IF_S2_2_IN_6_GA4(A, B, C, isNat_1_out_g1(A)) -> ISNAT_1_IN_G1(B)
IF_S2_2_IN_7_GA4(A, B, C, isNat_1_out_g1(B)) -> IF_S2_2_IN_8_GA4(A, B, C, add_3_in_gga3(A, B, C))
IF_S2_2_IN_7_GA4(A, B, C, isNat_1_out_g1(B)) -> ADD_3_IN_GGA3(A, B, C)
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> IF_ADD_3_IN_1_GGA4(X, Y, Z, add_3_in_gga3(X, Y, Z))
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> ADD_3_IN_GGA3(X, Y, Z)
IF_S2_2_IN_3_GA4(X, Y, Z, s2_2_out_ga2(X, A)) -> IF_S2_2_IN_4_GA5(X, Y, Z, A, s2_2_in_ga2(Y, B))
IF_S2_2_IN_3_GA4(X, Y, Z, s2_2_out_ga2(X, A)) -> S2_2_IN_GA2(Y, B)
IF_S2_2_IN_4_GA5(X, Y, Z, A, s2_2_out_ga2(Y, B)) -> IF_S2_2_IN_5_GA6(X, Y, Z, A, B, s2_2_in_ga2(plus_22(A, B), Z))
IF_S2_2_IN_4_GA5(X, Y, Z, A, s2_2_out_ga2(Y, B)) -> S2_2_IN_GA2(plus_22(A, B), Z)

The TRS R consists of the following rules:

s2_2_in_ga2(plus_22(A, plus_22(B, C)), D) -> if_s2_2_in_1_ga5(A, B, C, D, s2_2_in_ga2(plus_22(plus_22(A, B), C), D))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_2_ga4(A, B, C, s2_2_in_ga2(plus_22(B, A), C))
s2_2_in_ga2(plus_22(X, 0_0), X) -> s2_2_out_ga2(plus_22(X, 0_0), X)
s2_2_in_ga2(plus_22(X, Y), Z) -> if_s2_2_in_3_ga4(X, Y, Z, s2_2_in_ga2(X, A))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_6_ga4(A, B, C, isNat_1_in_g1(A))
isNat_1_in_g1(s_11(X)) -> if_isNat_1_in_1_g2(X, isNat_1_in_g1(X))
isNat_1_in_g1(0_0) -> isNat_1_out_g1(0_0)
if_isNat_1_in_1_g2(X, isNat_1_out_g1(X)) -> isNat_1_out_g1(s_11(X))
if_s2_2_in_6_ga4(A, B, C, isNat_1_out_g1(A)) -> if_s2_2_in_7_ga4(A, B, C, isNat_1_in_g1(B))
if_s2_2_in_7_ga4(A, B, C, isNat_1_out_g1(B)) -> if_s2_2_in_8_ga4(A, B, C, add_3_in_gga3(A, B, C))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_s2_2_in_8_ga4(A, B, C, add_3_out_gga3(A, B, C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_3_ga4(X, Y, Z, s2_2_out_ga2(X, A)) -> if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_in_ga2(Y, B))
if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_out_ga2(Y, B)) -> if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_in_ga2(plus_22(A, B), Z))
if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_out_ga2(plus_22(A, B), Z)) -> s2_2_out_ga2(plus_22(X, Y), Z)
if_s2_2_in_2_ga4(A, B, C, s2_2_out_ga2(plus_22(B, A), C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_1_ga5(A, B, C, D, s2_2_out_ga2(plus_22(plus_22(A, B), C), D)) -> s2_2_out_ga2(plus_22(A, plus_22(B, C)), D)

The argument filtering Pi contains the following mapping:
s2_2_in_ga2(x1, x2)  =  s2_2_in_ga1(x1)
plus_22(x1, x2)  =  plus_22(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
if_s2_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_1_ga1(x5)
if_s2_2_in_2_ga4(x1, x2, x3, x4)  =  if_s2_2_in_2_ga1(x4)
s2_2_out_ga2(x1, x2)  =  s2_2_out_ga1(x2)
if_s2_2_in_3_ga4(x1, x2, x3, x4)  =  if_s2_2_in_3_ga2(x2, x4)
if_s2_2_in_6_ga4(x1, x2, x3, x4)  =  if_s2_2_in_6_ga3(x1, x2, x4)
isNat_1_in_g1(x1)  =  isNat_1_in_g1(x1)
if_isNat_1_in_1_g2(x1, x2)  =  if_isNat_1_in_1_g1(x2)
isNat_1_out_g1(x1)  =  isNat_1_out_g
if_s2_2_in_7_ga4(x1, x2, x3, x4)  =  if_s2_2_in_7_ga3(x1, x2, x4)
if_s2_2_in_8_ga4(x1, x2, x3, x4)  =  if_s2_2_in_8_ga1(x4)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_s2_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_4_ga2(x4, x5)
if_s2_2_in_5_ga6(x1, x2, x3, x4, x5, x6)  =  if_s2_2_in_5_ga1(x6)
IF_S2_2_IN_3_GA4(x1, x2, x3, x4)  =  IF_S2_2_IN_3_GA2(x2, x4)
IF_S2_2_IN_6_GA4(x1, x2, x3, x4)  =  IF_S2_2_IN_6_GA3(x1, x2, x4)
ADD_3_IN_GGA3(x1, x2, x3)  =  ADD_3_IN_GGA2(x1, x2)
S2_2_IN_GA2(x1, x2)  =  S2_2_IN_GA1(x1)
IF_S2_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_S2_2_IN_1_GA1(x5)
IF_S2_2_IN_8_GA4(x1, x2, x3, x4)  =  IF_S2_2_IN_8_GA1(x4)
IF_S2_2_IN_2_GA4(x1, x2, x3, x4)  =  IF_S2_2_IN_2_GA1(x4)
IF_S2_2_IN_5_GA6(x1, x2, x3, x4, x5, x6)  =  IF_S2_2_IN_5_GA1(x6)
IF_ADD_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_ADD_3_IN_1_GGA1(x4)
ISNAT_1_IN_G1(x1)  =  ISNAT_1_IN_G1(x1)
IF_ISNAT_1_IN_1_G2(x1, x2)  =  IF_ISNAT_1_IN_1_G1(x2)
IF_S2_2_IN_7_GA4(x1, x2, x3, x4)  =  IF_S2_2_IN_7_GA3(x1, x2, x4)
IF_S2_2_IN_4_GA5(x1, x2, x3, x4, x5)  =  IF_S2_2_IN_4_GA2(x4, x5)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 3 SCCs with 11 less nodes.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> ADD_3_IN_GGA3(X, Y, Z)

The TRS R consists of the following rules:

s2_2_in_ga2(plus_22(A, plus_22(B, C)), D) -> if_s2_2_in_1_ga5(A, B, C, D, s2_2_in_ga2(plus_22(plus_22(A, B), C), D))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_2_ga4(A, B, C, s2_2_in_ga2(plus_22(B, A), C))
s2_2_in_ga2(plus_22(X, 0_0), X) -> s2_2_out_ga2(plus_22(X, 0_0), X)
s2_2_in_ga2(plus_22(X, Y), Z) -> if_s2_2_in_3_ga4(X, Y, Z, s2_2_in_ga2(X, A))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_6_ga4(A, B, C, isNat_1_in_g1(A))
isNat_1_in_g1(s_11(X)) -> if_isNat_1_in_1_g2(X, isNat_1_in_g1(X))
isNat_1_in_g1(0_0) -> isNat_1_out_g1(0_0)
if_isNat_1_in_1_g2(X, isNat_1_out_g1(X)) -> isNat_1_out_g1(s_11(X))
if_s2_2_in_6_ga4(A, B, C, isNat_1_out_g1(A)) -> if_s2_2_in_7_ga4(A, B, C, isNat_1_in_g1(B))
if_s2_2_in_7_ga4(A, B, C, isNat_1_out_g1(B)) -> if_s2_2_in_8_ga4(A, B, C, add_3_in_gga3(A, B, C))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_s2_2_in_8_ga4(A, B, C, add_3_out_gga3(A, B, C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_3_ga4(X, Y, Z, s2_2_out_ga2(X, A)) -> if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_in_ga2(Y, B))
if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_out_ga2(Y, B)) -> if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_in_ga2(plus_22(A, B), Z))
if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_out_ga2(plus_22(A, B), Z)) -> s2_2_out_ga2(plus_22(X, Y), Z)
if_s2_2_in_2_ga4(A, B, C, s2_2_out_ga2(plus_22(B, A), C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_1_ga5(A, B, C, D, s2_2_out_ga2(plus_22(plus_22(A, B), C), D)) -> s2_2_out_ga2(plus_22(A, plus_22(B, C)), D)

The argument filtering Pi contains the following mapping:
s2_2_in_ga2(x1, x2)  =  s2_2_in_ga1(x1)
plus_22(x1, x2)  =  plus_22(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
if_s2_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_1_ga1(x5)
if_s2_2_in_2_ga4(x1, x2, x3, x4)  =  if_s2_2_in_2_ga1(x4)
s2_2_out_ga2(x1, x2)  =  s2_2_out_ga1(x2)
if_s2_2_in_3_ga4(x1, x2, x3, x4)  =  if_s2_2_in_3_ga2(x2, x4)
if_s2_2_in_6_ga4(x1, x2, x3, x4)  =  if_s2_2_in_6_ga3(x1, x2, x4)
isNat_1_in_g1(x1)  =  isNat_1_in_g1(x1)
if_isNat_1_in_1_g2(x1, x2)  =  if_isNat_1_in_1_g1(x2)
isNat_1_out_g1(x1)  =  isNat_1_out_g
if_s2_2_in_7_ga4(x1, x2, x3, x4)  =  if_s2_2_in_7_ga3(x1, x2, x4)
if_s2_2_in_8_ga4(x1, x2, x3, x4)  =  if_s2_2_in_8_ga1(x4)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_s2_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_4_ga2(x4, x5)
if_s2_2_in_5_ga6(x1, x2, x3, x4, x5, x6)  =  if_s2_2_in_5_ga1(x6)
ADD_3_IN_GGA3(x1, x2, x3)  =  ADD_3_IN_GGA2(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> ADD_3_IN_GGA3(X, Y, Z)

R is empty.
The argument filtering Pi contains the following mapping:
s_11(x1)  =  s_11(x1)
ADD_3_IN_GGA3(x1, x2, x3)  =  ADD_3_IN_GGA2(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

ADD_3_IN_GGA2(s_11(X), Y) -> ADD_3_IN_GGA2(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {ADD_3_IN_GGA2}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

ISNAT_1_IN_G1(s_11(X)) -> ISNAT_1_IN_G1(X)

The TRS R consists of the following rules:

s2_2_in_ga2(plus_22(A, plus_22(B, C)), D) -> if_s2_2_in_1_ga5(A, B, C, D, s2_2_in_ga2(plus_22(plus_22(A, B), C), D))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_2_ga4(A, B, C, s2_2_in_ga2(plus_22(B, A), C))
s2_2_in_ga2(plus_22(X, 0_0), X) -> s2_2_out_ga2(plus_22(X, 0_0), X)
s2_2_in_ga2(plus_22(X, Y), Z) -> if_s2_2_in_3_ga4(X, Y, Z, s2_2_in_ga2(X, A))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_6_ga4(A, B, C, isNat_1_in_g1(A))
isNat_1_in_g1(s_11(X)) -> if_isNat_1_in_1_g2(X, isNat_1_in_g1(X))
isNat_1_in_g1(0_0) -> isNat_1_out_g1(0_0)
if_isNat_1_in_1_g2(X, isNat_1_out_g1(X)) -> isNat_1_out_g1(s_11(X))
if_s2_2_in_6_ga4(A, B, C, isNat_1_out_g1(A)) -> if_s2_2_in_7_ga4(A, B, C, isNat_1_in_g1(B))
if_s2_2_in_7_ga4(A, B, C, isNat_1_out_g1(B)) -> if_s2_2_in_8_ga4(A, B, C, add_3_in_gga3(A, B, C))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_s2_2_in_8_ga4(A, B, C, add_3_out_gga3(A, B, C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_3_ga4(X, Y, Z, s2_2_out_ga2(X, A)) -> if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_in_ga2(Y, B))
if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_out_ga2(Y, B)) -> if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_in_ga2(plus_22(A, B), Z))
if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_out_ga2(plus_22(A, B), Z)) -> s2_2_out_ga2(plus_22(X, Y), Z)
if_s2_2_in_2_ga4(A, B, C, s2_2_out_ga2(plus_22(B, A), C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_1_ga5(A, B, C, D, s2_2_out_ga2(plus_22(plus_22(A, B), C), D)) -> s2_2_out_ga2(plus_22(A, plus_22(B, C)), D)

The argument filtering Pi contains the following mapping:
s2_2_in_ga2(x1, x2)  =  s2_2_in_ga1(x1)
plus_22(x1, x2)  =  plus_22(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
if_s2_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_1_ga1(x5)
if_s2_2_in_2_ga4(x1, x2, x3, x4)  =  if_s2_2_in_2_ga1(x4)
s2_2_out_ga2(x1, x2)  =  s2_2_out_ga1(x2)
if_s2_2_in_3_ga4(x1, x2, x3, x4)  =  if_s2_2_in_3_ga2(x2, x4)
if_s2_2_in_6_ga4(x1, x2, x3, x4)  =  if_s2_2_in_6_ga3(x1, x2, x4)
isNat_1_in_g1(x1)  =  isNat_1_in_g1(x1)
if_isNat_1_in_1_g2(x1, x2)  =  if_isNat_1_in_1_g1(x2)
isNat_1_out_g1(x1)  =  isNat_1_out_g
if_s2_2_in_7_ga4(x1, x2, x3, x4)  =  if_s2_2_in_7_ga3(x1, x2, x4)
if_s2_2_in_8_ga4(x1, x2, x3, x4)  =  if_s2_2_in_8_ga1(x4)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_s2_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_4_ga2(x4, x5)
if_s2_2_in_5_ga6(x1, x2, x3, x4, x5, x6)  =  if_s2_2_in_5_ga1(x6)
ISNAT_1_IN_G1(x1)  =  ISNAT_1_IN_G1(x1)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

ISNAT_1_IN_G1(s_11(X)) -> ISNAT_1_IN_G1(X)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

ISNAT_1_IN_G1(s_11(X)) -> ISNAT_1_IN_G1(X)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {ISNAT_1_IN_G1}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

IF_S2_2_IN_4_GA5(X, Y, Z, A, s2_2_out_ga2(Y, B)) -> S2_2_IN_GA2(plus_22(A, B), Z)
IF_S2_2_IN_3_GA4(X, Y, Z, s2_2_out_ga2(X, A)) -> S2_2_IN_GA2(Y, B)
S2_2_IN_GA2(plus_22(X, Y), Z) -> IF_S2_2_IN_3_GA4(X, Y, Z, s2_2_in_ga2(X, A))
S2_2_IN_GA2(plus_22(A, plus_22(B, C)), D) -> S2_2_IN_GA2(plus_22(plus_22(A, B), C), D)
S2_2_IN_GA2(plus_22(X, Y), Z) -> S2_2_IN_GA2(X, A)
S2_2_IN_GA2(plus_22(A, B), C) -> S2_2_IN_GA2(plus_22(B, A), C)
IF_S2_2_IN_3_GA4(X, Y, Z, s2_2_out_ga2(X, A)) -> IF_S2_2_IN_4_GA5(X, Y, Z, A, s2_2_in_ga2(Y, B))

The TRS R consists of the following rules:

s2_2_in_ga2(plus_22(A, plus_22(B, C)), D) -> if_s2_2_in_1_ga5(A, B, C, D, s2_2_in_ga2(plus_22(plus_22(A, B), C), D))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_2_ga4(A, B, C, s2_2_in_ga2(plus_22(B, A), C))
s2_2_in_ga2(plus_22(X, 0_0), X) -> s2_2_out_ga2(plus_22(X, 0_0), X)
s2_2_in_ga2(plus_22(X, Y), Z) -> if_s2_2_in_3_ga4(X, Y, Z, s2_2_in_ga2(X, A))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_6_ga4(A, B, C, isNat_1_in_g1(A))
isNat_1_in_g1(s_11(X)) -> if_isNat_1_in_1_g2(X, isNat_1_in_g1(X))
isNat_1_in_g1(0_0) -> isNat_1_out_g1(0_0)
if_isNat_1_in_1_g2(X, isNat_1_out_g1(X)) -> isNat_1_out_g1(s_11(X))
if_s2_2_in_6_ga4(A, B, C, isNat_1_out_g1(A)) -> if_s2_2_in_7_ga4(A, B, C, isNat_1_in_g1(B))
if_s2_2_in_7_ga4(A, B, C, isNat_1_out_g1(B)) -> if_s2_2_in_8_ga4(A, B, C, add_3_in_gga3(A, B, C))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_s2_2_in_8_ga4(A, B, C, add_3_out_gga3(A, B, C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_3_ga4(X, Y, Z, s2_2_out_ga2(X, A)) -> if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_in_ga2(Y, B))
if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_out_ga2(Y, B)) -> if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_in_ga2(plus_22(A, B), Z))
if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_out_ga2(plus_22(A, B), Z)) -> s2_2_out_ga2(plus_22(X, Y), Z)
if_s2_2_in_2_ga4(A, B, C, s2_2_out_ga2(plus_22(B, A), C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_1_ga5(A, B, C, D, s2_2_out_ga2(plus_22(plus_22(A, B), C), D)) -> s2_2_out_ga2(plus_22(A, plus_22(B, C)), D)

The argument filtering Pi contains the following mapping:
s2_2_in_ga2(x1, x2)  =  s2_2_in_ga1(x1)
plus_22(x1, x2)  =  plus_22(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
if_s2_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_1_ga1(x5)
if_s2_2_in_2_ga4(x1, x2, x3, x4)  =  if_s2_2_in_2_ga1(x4)
s2_2_out_ga2(x1, x2)  =  s2_2_out_ga1(x2)
if_s2_2_in_3_ga4(x1, x2, x3, x4)  =  if_s2_2_in_3_ga2(x2, x4)
if_s2_2_in_6_ga4(x1, x2, x3, x4)  =  if_s2_2_in_6_ga3(x1, x2, x4)
isNat_1_in_g1(x1)  =  isNat_1_in_g1(x1)
if_isNat_1_in_1_g2(x1, x2)  =  if_isNat_1_in_1_g1(x2)
isNat_1_out_g1(x1)  =  isNat_1_out_g
if_s2_2_in_7_ga4(x1, x2, x3, x4)  =  if_s2_2_in_7_ga3(x1, x2, x4)
if_s2_2_in_8_ga4(x1, x2, x3, x4)  =  if_s2_2_in_8_ga1(x4)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_s2_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_4_ga2(x4, x5)
if_s2_2_in_5_ga6(x1, x2, x3, x4, x5, x6)  =  if_s2_2_in_5_ga1(x6)
IF_S2_2_IN_3_GA4(x1, x2, x3, x4)  =  IF_S2_2_IN_3_GA2(x2, x4)
S2_2_IN_GA2(x1, x2)  =  S2_2_IN_GA1(x1)
IF_S2_2_IN_4_GA5(x1, x2, x3, x4, x5)  =  IF_S2_2_IN_4_GA2(x4, x5)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

IF_S2_2_IN_4_GA2(A, s2_2_out_ga1(B)) -> S2_2_IN_GA1(plus_22(A, B))
IF_S2_2_IN_3_GA2(Y, s2_2_out_ga1(A)) -> S2_2_IN_GA1(Y)
S2_2_IN_GA1(plus_22(X, Y)) -> IF_S2_2_IN_3_GA2(Y, s2_2_in_ga1(X))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))
S2_2_IN_GA1(plus_22(X, Y)) -> S2_2_IN_GA1(X)
S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
IF_S2_2_IN_3_GA2(Y, s2_2_out_ga1(A)) -> IF_S2_2_IN_4_GA2(A, s2_2_in_ga1(Y))

The TRS R consists of the following rules:

s2_2_in_ga1(plus_22(A, plus_22(B, C))) -> if_s2_2_in_1_ga1(s2_2_in_ga1(plus_22(plus_22(A, B), C)))
s2_2_in_ga1(plus_22(A, B)) -> if_s2_2_in_2_ga1(s2_2_in_ga1(plus_22(B, A)))
s2_2_in_ga1(plus_22(X, 0_0)) -> s2_2_out_ga1(X)
s2_2_in_ga1(plus_22(X, Y)) -> if_s2_2_in_3_ga2(Y, s2_2_in_ga1(X))
s2_2_in_ga1(plus_22(A, B)) -> if_s2_2_in_6_ga3(A, B, isNat_1_in_g1(A))
isNat_1_in_g1(s_11(X)) -> if_isNat_1_in_1_g1(isNat_1_in_g1(X))
isNat_1_in_g1(0_0) -> isNat_1_out_g
if_isNat_1_in_1_g1(isNat_1_out_g) -> isNat_1_out_g
if_s2_2_in_6_ga3(A, B, isNat_1_out_g) -> if_s2_2_in_7_ga3(A, B, isNat_1_in_g1(B))
if_s2_2_in_7_ga3(A, B, isNat_1_out_g) -> if_s2_2_in_8_ga1(add_3_in_gga2(A, B))
add_3_in_gga2(s_11(X), Y) -> if_add_3_in_1_gga1(add_3_in_gga2(X, Y))
add_3_in_gga2(0_0, X) -> add_3_out_gga1(X)
if_add_3_in_1_gga1(add_3_out_gga1(Z)) -> add_3_out_gga1(s_11(Z))
if_s2_2_in_8_ga1(add_3_out_gga1(C)) -> s2_2_out_ga1(C)
if_s2_2_in_3_ga2(Y, s2_2_out_ga1(A)) -> if_s2_2_in_4_ga2(A, s2_2_in_ga1(Y))
if_s2_2_in_4_ga2(A, s2_2_out_ga1(B)) -> if_s2_2_in_5_ga1(s2_2_in_ga1(plus_22(A, B)))
if_s2_2_in_5_ga1(s2_2_out_ga1(Z)) -> s2_2_out_ga1(Z)
if_s2_2_in_2_ga1(s2_2_out_ga1(C)) -> s2_2_out_ga1(C)
if_s2_2_in_1_ga1(s2_2_out_ga1(D)) -> s2_2_out_ga1(D)

The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1, IF_S2_2_IN_4_GA2, IF_S2_2_IN_3_GA2}.
By using a polynomial ordering, the following set of Dependency Pairs of this DP problem can be strictly oriented.

IF_S2_2_IN_4_GA2(A, s2_2_out_ga1(B)) -> S2_2_IN_GA1(plus_22(A, B))
IF_S2_2_IN_3_GA2(Y, s2_2_out_ga1(A)) -> S2_2_IN_GA1(Y)
IF_S2_2_IN_3_GA2(Y, s2_2_out_ga1(A)) -> IF_S2_2_IN_4_GA2(A, s2_2_in_ga1(Y))
The remaining Dependency Pairs were at least non-strictly be oriented.

S2_2_IN_GA1(plus_22(X, Y)) -> IF_S2_2_IN_3_GA2(Y, s2_2_in_ga1(X))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))
S2_2_IN_GA1(plus_22(X, Y)) -> S2_2_IN_GA1(X)
S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
With the implicit AFS we had to orient the following set of usable rules non-strictly.

if_s2_2_in_4_ga2(A, s2_2_out_ga1(B)) -> if_s2_2_in_5_ga1(s2_2_in_ga1(plus_22(A, B)))
s2_2_in_ga1(plus_22(A, plus_22(B, C))) -> if_s2_2_in_1_ga1(s2_2_in_ga1(plus_22(plus_22(A, B), C)))
add_3_in_gga2(0_0, X) -> add_3_out_gga1(X)
if_s2_2_in_3_ga2(Y, s2_2_out_ga1(A)) -> if_s2_2_in_4_ga2(A, s2_2_in_ga1(Y))
s2_2_in_ga1(plus_22(A, B)) -> if_s2_2_in_6_ga3(A, B, isNat_1_in_g1(A))
if_add_3_in_1_gga1(add_3_out_gga1(Z)) -> add_3_out_gga1(s_11(Z))
if_s2_2_in_8_ga1(add_3_out_gga1(C)) -> s2_2_out_ga1(C)
if_s2_2_in_6_ga3(A, B, isNat_1_out_g) -> if_s2_2_in_7_ga3(A, B, isNat_1_in_g1(B))
if_s2_2_in_1_ga1(s2_2_out_ga1(D)) -> s2_2_out_ga1(D)
s2_2_in_ga1(plus_22(X, Y)) -> if_s2_2_in_3_ga2(Y, s2_2_in_ga1(X))
if_s2_2_in_7_ga3(A, B, isNat_1_out_g) -> if_s2_2_in_8_ga1(add_3_in_gga2(A, B))
s2_2_in_ga1(plus_22(X, 0_0)) -> s2_2_out_ga1(X)
if_s2_2_in_2_ga1(s2_2_out_ga1(C)) -> s2_2_out_ga1(C)
if_s2_2_in_5_ga1(s2_2_out_ga1(Z)) -> s2_2_out_ga1(Z)
add_3_in_gga2(s_11(X), Y) -> if_add_3_in_1_gga1(add_3_in_gga2(X, Y))
s2_2_in_ga1(plus_22(A, B)) -> if_s2_2_in_2_ga1(s2_2_in_ga1(plus_22(B, A)))
Used ordering: POLO with Polynomial interpretation:

POL(0_0) = 1   
POL(IF_S2_2_IN_3_GA2(x1, x2)) = x1 + x2   
POL(if_s2_2_in_4_ga2(x1, x2)) = x1 + x2   
POL(if_s2_2_in_2_ga1(x1)) = x1   
POL(if_s2_2_in_3_ga2(x1, x2)) = x1 + x2   
POL(if_s2_2_in_7_ga3(x1, x2, x3)) = x1 + x2   
POL(if_add_3_in_1_gga1(x1)) = x1   
POL(add_3_out_gga1(x1)) = 1 + x1   
POL(if_isNat_1_in_1_g1(x1)) = 0   
POL(isNat_1_out_g) = 0   
POL(s2_2_out_ga1(x1)) = 1 + x1   
POL(IF_S2_2_IN_4_GA2(x1, x2)) = x1 + x2   
POL(if_s2_2_in_5_ga1(x1)) = x1   
POL(if_s2_2_in_6_ga3(x1, x2, x3)) = x1 + x2   
POL(isNat_1_in_g1(x1)) = 0   
POL(add_3_in_gga2(x1, x2)) = x1 + x2   
POL(if_s2_2_in_8_ga1(x1)) = x1   
POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = x1   
POL(s_11(x1)) = x1   
POL(if_s2_2_in_1_ga1(x1)) = x1   
POL(s2_2_in_ga1(x1)) = x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(X, Y)) -> IF_S2_2_IN_3_GA2(Y, s2_2_in_ga1(X))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))
S2_2_IN_GA1(plus_22(X, Y)) -> S2_2_IN_GA1(X)
S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))

The TRS R consists of the following rules:

s2_2_in_ga1(plus_22(A, plus_22(B, C))) -> if_s2_2_in_1_ga1(s2_2_in_ga1(plus_22(plus_22(A, B), C)))
s2_2_in_ga1(plus_22(A, B)) -> if_s2_2_in_2_ga1(s2_2_in_ga1(plus_22(B, A)))
s2_2_in_ga1(plus_22(X, 0_0)) -> s2_2_out_ga1(X)
s2_2_in_ga1(plus_22(X, Y)) -> if_s2_2_in_3_ga2(Y, s2_2_in_ga1(X))
s2_2_in_ga1(plus_22(A, B)) -> if_s2_2_in_6_ga3(A, B, isNat_1_in_g1(A))
isNat_1_in_g1(s_11(X)) -> if_isNat_1_in_1_g1(isNat_1_in_g1(X))
isNat_1_in_g1(0_0) -> isNat_1_out_g
if_isNat_1_in_1_g1(isNat_1_out_g) -> isNat_1_out_g
if_s2_2_in_6_ga3(A, B, isNat_1_out_g) -> if_s2_2_in_7_ga3(A, B, isNat_1_in_g1(B))
if_s2_2_in_7_ga3(A, B, isNat_1_out_g) -> if_s2_2_in_8_ga1(add_3_in_gga2(A, B))
add_3_in_gga2(s_11(X), Y) -> if_add_3_in_1_gga1(add_3_in_gga2(X, Y))
add_3_in_gga2(0_0, X) -> add_3_out_gga1(X)
if_add_3_in_1_gga1(add_3_out_gga1(Z)) -> add_3_out_gga1(s_11(Z))
if_s2_2_in_8_ga1(add_3_out_gga1(C)) -> s2_2_out_ga1(C)
if_s2_2_in_3_ga2(Y, s2_2_out_ga1(A)) -> if_s2_2_in_4_ga2(A, s2_2_in_ga1(Y))
if_s2_2_in_4_ga2(A, s2_2_out_ga1(B)) -> if_s2_2_in_5_ga1(s2_2_in_ga1(plus_22(A, B)))
if_s2_2_in_5_ga1(s2_2_out_ga1(Z)) -> s2_2_out_ga1(Z)
if_s2_2_in_2_ga1(s2_2_out_ga1(C)) -> s2_2_out_ga1(C)
if_s2_2_in_1_ga1(s2_2_out_ga1(D)) -> s2_2_out_ga1(D)

The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_S2_2_IN_3_GA2, S2_2_IN_GA1}.
The approximation of the Dependency Graph contains 1 SCC with 1 less node.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(X, Y)) -> S2_2_IN_GA1(X)
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

The TRS R consists of the following rules:

s2_2_in_ga1(plus_22(A, plus_22(B, C))) -> if_s2_2_in_1_ga1(s2_2_in_ga1(plus_22(plus_22(A, B), C)))
s2_2_in_ga1(plus_22(A, B)) -> if_s2_2_in_2_ga1(s2_2_in_ga1(plus_22(B, A)))
s2_2_in_ga1(plus_22(X, 0_0)) -> s2_2_out_ga1(X)
s2_2_in_ga1(plus_22(X, Y)) -> if_s2_2_in_3_ga2(Y, s2_2_in_ga1(X))
s2_2_in_ga1(plus_22(A, B)) -> if_s2_2_in_6_ga3(A, B, isNat_1_in_g1(A))
isNat_1_in_g1(s_11(X)) -> if_isNat_1_in_1_g1(isNat_1_in_g1(X))
isNat_1_in_g1(0_0) -> isNat_1_out_g
if_isNat_1_in_1_g1(isNat_1_out_g) -> isNat_1_out_g
if_s2_2_in_6_ga3(A, B, isNat_1_out_g) -> if_s2_2_in_7_ga3(A, B, isNat_1_in_g1(B))
if_s2_2_in_7_ga3(A, B, isNat_1_out_g) -> if_s2_2_in_8_ga1(add_3_in_gga2(A, B))
add_3_in_gga2(s_11(X), Y) -> if_add_3_in_1_gga1(add_3_in_gga2(X, Y))
add_3_in_gga2(0_0, X) -> add_3_out_gga1(X)
if_add_3_in_1_gga1(add_3_out_gga1(Z)) -> add_3_out_gga1(s_11(Z))
if_s2_2_in_8_ga1(add_3_out_gga1(C)) -> s2_2_out_ga1(C)
if_s2_2_in_3_ga2(Y, s2_2_out_ga1(A)) -> if_s2_2_in_4_ga2(A, s2_2_in_ga1(Y))
if_s2_2_in_4_ga2(A, s2_2_out_ga1(B)) -> if_s2_2_in_5_ga1(s2_2_in_ga1(plus_22(A, B)))
if_s2_2_in_5_ga1(s2_2_out_ga1(Z)) -> s2_2_out_ga1(Z)
if_s2_2_in_2_ga1(s2_2_out_ga1(C)) -> s2_2_out_ga1(C)
if_s2_2_in_1_ga1(s2_2_out_ga1(D)) -> s2_2_out_ga1(D)

The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(X, Y)) -> S2_2_IN_GA1(X)
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(X, Y)) -> S2_2_IN_GA1(X)
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(X, Y)) -> S2_2_IN_GA1(X)
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(X, Y)) -> S2_2_IN_GA1(X)
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(X, Y)) -> S2_2_IN_GA1(X)
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(X, Y)) -> S2_2_IN_GA1(X)
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(X, Y)) -> S2_2_IN_GA1(X)
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(X, Y)) -> S2_2_IN_GA1(X)
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(X, Y)) -> S2_2_IN_GA1(X)
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, the following set of Dependency Pairs of this DP problem can be strictly oriented.

S2_2_IN_GA1(plus_22(X, Y)) -> S2_2_IN_GA1(X)
The remaining Dependency Pairs were at least non-strictly be oriented.

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))
With the implicit AFS there is no usable rule.

Used ordering: POLO with Polynomial interpretation:


POL(plus_22(x1, x2)) = 1 + x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
                                                                                      ↳ QDP
                                                                                        ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
                                                                                      ↳ QDP
                                                                                        ↳ RuleRemovalProof
                                                                                          ↳ QDP
                                                                                            ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
                                                                                      ↳ QDP
                                                                                        ↳ RuleRemovalProof
                                                                                          ↳ QDP
                                                                                            ↳ RuleRemovalProof
                                                                                              ↳ QDP
                                                                                                ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
                                                                                      ↳ QDP
                                                                                        ↳ RuleRemovalProof
                                                                                          ↳ QDP
                                                                                            ↳ RuleRemovalProof
                                                                                              ↳ QDP
                                                                                                ↳ RuleRemovalProof
                                                                                                  ↳ QDP
                                                                                                    ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
                                                                                      ↳ QDP
                                                                                        ↳ RuleRemovalProof
                                                                                          ↳ QDP
                                                                                            ↳ RuleRemovalProof
                                                                                              ↳ QDP
                                                                                                ↳ RuleRemovalProof
                                                                                                  ↳ QDP
                                                                                                    ↳ RuleRemovalProof
                                                                                                      ↳ QDP
                                                                                                        ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
                                                                                      ↳ QDP
                                                                                        ↳ RuleRemovalProof
                                                                                          ↳ QDP
                                                                                            ↳ RuleRemovalProof
                                                                                              ↳ QDP
                                                                                                ↳ RuleRemovalProof
                                                                                                  ↳ QDP
                                                                                                    ↳ RuleRemovalProof
                                                                                                      ↳ QDP
                                                                                                        ↳ RuleRemovalProof
                                                                                                          ↳ QDP
                                                                                                            ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
                                                                                      ↳ QDP
                                                                                        ↳ RuleRemovalProof
                                                                                          ↳ QDP
                                                                                            ↳ RuleRemovalProof
                                                                                              ↳ QDP
                                                                                                ↳ RuleRemovalProof
                                                                                                  ↳ QDP
                                                                                                    ↳ RuleRemovalProof
                                                                                                      ↳ QDP
                                                                                                        ↳ RuleRemovalProof
                                                                                                          ↳ QDP
                                                                                                            ↳ RuleRemovalProof
                                                                                                              ↳ QDP
                                                                                                                ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
                                                                                      ↳ QDP
                                                                                        ↳ RuleRemovalProof
                                                                                          ↳ QDP
                                                                                            ↳ RuleRemovalProof
                                                                                              ↳ QDP
                                                                                                ↳ RuleRemovalProof
                                                                                                  ↳ QDP
                                                                                                    ↳ RuleRemovalProof
                                                                                                      ↳ QDP
                                                                                                        ↳ RuleRemovalProof
                                                                                                          ↳ QDP
                                                                                                            ↳ RuleRemovalProof
                                                                                                              ↳ QDP
                                                                                                                ↳ RuleRemovalProof
                                                                                                                  ↳ QDP
                                                                                                                    ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
                                                                                      ↳ QDP
                                                                                        ↳ RuleRemovalProof
                                                                                          ↳ QDP
                                                                                            ↳ RuleRemovalProof
                                                                                              ↳ QDP
                                                                                                ↳ RuleRemovalProof
                                                                                                  ↳ QDP
                                                                                                    ↳ RuleRemovalProof
                                                                                                      ↳ QDP
                                                                                                        ↳ RuleRemovalProof
                                                                                                          ↳ QDP
                                                                                                            ↳ RuleRemovalProof
                                                                                                              ↳ QDP
                                                                                                                ↳ RuleRemovalProof
                                                                                                                  ↳ QDP
                                                                                                                    ↳ RuleRemovalProof
                                                                                                                      ↳ QDP
                                                                                                                        ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
                                                                                      ↳ QDP
                                                                                        ↳ RuleRemovalProof
                                                                                          ↳ QDP
                                                                                            ↳ RuleRemovalProof
                                                                                              ↳ QDP
                                                                                                ↳ RuleRemovalProof
                                                                                                  ↳ QDP
                                                                                                    ↳ RuleRemovalProof
                                                                                                      ↳ QDP
                                                                                                        ↳ RuleRemovalProof
                                                                                                          ↳ QDP
                                                                                                            ↳ RuleRemovalProof
                                                                                                              ↳ QDP
                                                                                                                ↳ RuleRemovalProof
                                                                                                                  ↳ QDP
                                                                                                                    ↳ RuleRemovalProof
                                                                                                                      ↳ QDP
                                                                                                                        ↳ RuleRemovalProof
                                                                                                                          ↳ QDP
                                                                                                                            ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
                                                                                      ↳ QDP
                                                                                        ↳ RuleRemovalProof
                                                                                          ↳ QDP
                                                                                            ↳ RuleRemovalProof
                                                                                              ↳ QDP
                                                                                                ↳ RuleRemovalProof
                                                                                                  ↳ QDP
                                                                                                    ↳ RuleRemovalProof
                                                                                                      ↳ QDP
                                                                                                        ↳ RuleRemovalProof
                                                                                                          ↳ QDP
                                                                                                            ↳ RuleRemovalProof
                                                                                                              ↳ QDP
                                                                                                                ↳ RuleRemovalProof
                                                                                                                  ↳ QDP
                                                                                                                    ↳ RuleRemovalProof
                                                                                                                      ↳ QDP
                                                                                                                        ↳ RuleRemovalProof
                                                                                                                          ↳ QDP
                                                                                                                            ↳ RuleRemovalProof
                                                                                                                              ↳ QDP
                                                                                                                                ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
                                                                                      ↳ QDP
                                                                                        ↳ RuleRemovalProof
                                                                                          ↳ QDP
                                                                                            ↳ RuleRemovalProof
                                                                                              ↳ QDP
                                                                                                ↳ RuleRemovalProof
                                                                                                  ↳ QDP
                                                                                                    ↳ RuleRemovalProof
                                                                                                      ↳ QDP
                                                                                                        ↳ RuleRemovalProof
                                                                                                          ↳ QDP
                                                                                                            ↳ RuleRemovalProof
                                                                                                              ↳ QDP
                                                                                                                ↳ RuleRemovalProof
                                                                                                                  ↳ QDP
                                                                                                                    ↳ RuleRemovalProof
                                                                                                                      ↳ QDP
                                                                                                                        ↳ RuleRemovalProof
                                                                                                                          ↳ QDP
                                                                                                                            ↳ RuleRemovalProof
                                                                                                                              ↳ QDP
                                                                                                                                ↳ RuleRemovalProof
                                                                                                                                  ↳ QDP
                                                                                                                                    ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
                                                                                      ↳ QDP
                                                                                        ↳ RuleRemovalProof
                                                                                          ↳ QDP
                                                                                            ↳ RuleRemovalProof
                                                                                              ↳ QDP
                                                                                                ↳ RuleRemovalProof
                                                                                                  ↳ QDP
                                                                                                    ↳ RuleRemovalProof
                                                                                                      ↳ QDP
                                                                                                        ↳ RuleRemovalProof
                                                                                                          ↳ QDP
                                                                                                            ↳ RuleRemovalProof
                                                                                                              ↳ QDP
                                                                                                                ↳ RuleRemovalProof
                                                                                                                  ↳ QDP
                                                                                                                    ↳ RuleRemovalProof
                                                                                                                      ↳ QDP
                                                                                                                        ↳ RuleRemovalProof
                                                                                                                          ↳ QDP
                                                                                                                            ↳ RuleRemovalProof
                                                                                                                              ↳ QDP
                                                                                                                                ↳ RuleRemovalProof
                                                                                                                                  ↳ QDP
                                                                                                                                    ↳ RuleRemovalProof
                                                                                                                                      ↳ QDP
                                                                                                                                        ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
                                                                                      ↳ QDP
                                                                                        ↳ RuleRemovalProof
                                                                                          ↳ QDP
                                                                                            ↳ RuleRemovalProof
                                                                                              ↳ QDP
                                                                                                ↳ RuleRemovalProof
                                                                                                  ↳ QDP
                                                                                                    ↳ RuleRemovalProof
                                                                                                      ↳ QDP
                                                                                                        ↳ RuleRemovalProof
                                                                                                          ↳ QDP
                                                                                                            ↳ RuleRemovalProof
                                                                                                              ↳ QDP
                                                                                                                ↳ RuleRemovalProof
                                                                                                                  ↳ QDP
                                                                                                                    ↳ RuleRemovalProof
                                                                                                                      ↳ QDP
                                                                                                                        ↳ RuleRemovalProof
                                                                                                                          ↳ QDP
                                                                                                                            ↳ RuleRemovalProof
                                                                                                                              ↳ QDP
                                                                                                                                ↳ RuleRemovalProof
                                                                                                                                  ↳ QDP
                                                                                                                                    ↳ RuleRemovalProof
                                                                                                                                      ↳ QDP
                                                                                                                                        ↳ RuleRemovalProof
                                                                                                                                          ↳ QDP
                                                                                                                                            ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
                                                                                      ↳ QDP
                                                                                        ↳ RuleRemovalProof
                                                                                          ↳ QDP
                                                                                            ↳ RuleRemovalProof
                                                                                              ↳ QDP
                                                                                                ↳ RuleRemovalProof
                                                                                                  ↳ QDP
                                                                                                    ↳ RuleRemovalProof
                                                                                                      ↳ QDP
                                                                                                        ↳ RuleRemovalProof
                                                                                                          ↳ QDP
                                                                                                            ↳ RuleRemovalProof
                                                                                                              ↳ QDP
                                                                                                                ↳ RuleRemovalProof
                                                                                                                  ↳ QDP
                                                                                                                    ↳ RuleRemovalProof
                                                                                                                      ↳ QDP
                                                                                                                        ↳ RuleRemovalProof
                                                                                                                          ↳ QDP
                                                                                                                            ↳ RuleRemovalProof
                                                                                                                              ↳ QDP
                                                                                                                                ↳ RuleRemovalProof
                                                                                                                                  ↳ QDP
                                                                                                                                    ↳ RuleRemovalProof
                                                                                                                                      ↳ QDP
                                                                                                                                        ↳ RuleRemovalProof
                                                                                                                                          ↳ QDP
                                                                                                                                            ↳ RuleRemovalProof
                                                                                                                                              ↳ QDP
                                                                                                                                                ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
                                                                                      ↳ QDP
                                                                                        ↳ RuleRemovalProof
                                                                                          ↳ QDP
                                                                                            ↳ RuleRemovalProof
                                                                                              ↳ QDP
                                                                                                ↳ RuleRemovalProof
                                                                                                  ↳ QDP
                                                                                                    ↳ RuleRemovalProof
                                                                                                      ↳ QDP
                                                                                                        ↳ RuleRemovalProof
                                                                                                          ↳ QDP
                                                                                                            ↳ RuleRemovalProof
                                                                                                              ↳ QDP
                                                                                                                ↳ RuleRemovalProof
                                                                                                                  ↳ QDP
                                                                                                                    ↳ RuleRemovalProof
                                                                                                                      ↳ QDP
                                                                                                                        ↳ RuleRemovalProof
                                                                                                                          ↳ QDP
                                                                                                                            ↳ RuleRemovalProof
                                                                                                                              ↳ QDP
                                                                                                                                ↳ RuleRemovalProof
                                                                                                                                  ↳ QDP
                                                                                                                                    ↳ RuleRemovalProof
                                                                                                                                      ↳ QDP
                                                                                                                                        ↳ RuleRemovalProof
                                                                                                                                          ↳ QDP
                                                                                                                                            ↳ RuleRemovalProof
                                                                                                                                              ↳ QDP
                                                                                                                                                ↳ RuleRemovalProof
                                                                                                                                                  ↳ QDP
                                                                                                                                                    ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
                                                                                      ↳ QDP
                                                                                        ↳ RuleRemovalProof
                                                                                          ↳ QDP
                                                                                            ↳ RuleRemovalProof
                                                                                              ↳ QDP
                                                                                                ↳ RuleRemovalProof
                                                                                                  ↳ QDP
                                                                                                    ↳ RuleRemovalProof
                                                                                                      ↳ QDP
                                                                                                        ↳ RuleRemovalProof
                                                                                                          ↳ QDP
                                                                                                            ↳ RuleRemovalProof
                                                                                                              ↳ QDP
                                                                                                                ↳ RuleRemovalProof
                                                                                                                  ↳ QDP
                                                                                                                    ↳ RuleRemovalProof
                                                                                                                      ↳ QDP
                                                                                                                        ↳ RuleRemovalProof
                                                                                                                          ↳ QDP
                                                                                                                            ↳ RuleRemovalProof
                                                                                                                              ↳ QDP
                                                                                                                                ↳ RuleRemovalProof
                                                                                                                                  ↳ QDP
                                                                                                                                    ↳ RuleRemovalProof
                                                                                                                                      ↳ QDP
                                                                                                                                        ↳ RuleRemovalProof
                                                                                                                                          ↳ QDP
                                                                                                                                            ↳ RuleRemovalProof
                                                                                                                                              ↳ QDP
                                                                                                                                                ↳ RuleRemovalProof
                                                                                                                                                  ↳ QDP
                                                                                                                                                    ↳ RuleRemovalProof
                                                                                                                                                      ↳ QDP
                                                                                                                                                        ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
                                                                                      ↳ QDP
                                                                                        ↳ RuleRemovalProof
                                                                                          ↳ QDP
                                                                                            ↳ RuleRemovalProof
                                                                                              ↳ QDP
                                                                                                ↳ RuleRemovalProof
                                                                                                  ↳ QDP
                                                                                                    ↳ RuleRemovalProof
                                                                                                      ↳ QDP
                                                                                                        ↳ RuleRemovalProof
                                                                                                          ↳ QDP
                                                                                                            ↳ RuleRemovalProof
                                                                                                              ↳ QDP
                                                                                                                ↳ RuleRemovalProof
                                                                                                                  ↳ QDP
                                                                                                                    ↳ RuleRemovalProof
                                                                                                                      ↳ QDP
                                                                                                                        ↳ RuleRemovalProof
                                                                                                                          ↳ QDP
                                                                                                                            ↳ RuleRemovalProof
                                                                                                                              ↳ QDP
                                                                                                                                ↳ RuleRemovalProof
                                                                                                                                  ↳ QDP
                                                                                                                                    ↳ RuleRemovalProof
                                                                                                                                      ↳ QDP
                                                                                                                                        ↳ RuleRemovalProof
                                                                                                                                          ↳ QDP
                                                                                                                                            ↳ RuleRemovalProof
                                                                                                                                              ↳ QDP
                                                                                                                                                ↳ RuleRemovalProof
                                                                                                                                                  ↳ QDP
                                                                                                                                                    ↳ RuleRemovalProof
                                                                                                                                                      ↳ QDP
                                                                                                                                                        ↳ RuleRemovalProof
                                                                                                                                                          ↳ QDP
                                                                                                                                                            ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
                                                                                      ↳ QDP
                                                                                        ↳ RuleRemovalProof
                                                                                          ↳ QDP
                                                                                            ↳ RuleRemovalProof
                                                                                              ↳ QDP
                                                                                                ↳ RuleRemovalProof
                                                                                                  ↳ QDP
                                                                                                    ↳ RuleRemovalProof
                                                                                                      ↳ QDP
                                                                                                        ↳ RuleRemovalProof
                                                                                                          ↳ QDP
                                                                                                            ↳ RuleRemovalProof
                                                                                                              ↳ QDP
                                                                                                                ↳ RuleRemovalProof
                                                                                                                  ↳ QDP
                                                                                                                    ↳ RuleRemovalProof
                                                                                                                      ↳ QDP
                                                                                                                        ↳ RuleRemovalProof
                                                                                                                          ↳ QDP
                                                                                                                            ↳ RuleRemovalProof
                                                                                                                              ↳ QDP
                                                                                                                                ↳ RuleRemovalProof
                                                                                                                                  ↳ QDP
                                                                                                                                    ↳ RuleRemovalProof
                                                                                                                                      ↳ QDP
                                                                                                                                        ↳ RuleRemovalProof
                                                                                                                                          ↳ QDP
                                                                                                                                            ↳ RuleRemovalProof
                                                                                                                                              ↳ QDP
                                                                                                                                                ↳ RuleRemovalProof
                                                                                                                                                  ↳ QDP
                                                                                                                                                    ↳ RuleRemovalProof
                                                                                                                                                      ↳ QDP
                                                                                                                                                        ↳ RuleRemovalProof
                                                                                                                                                          ↳ QDP
                                                                                                                                                            ↳ RuleRemovalProof
                                                                                                                                                              ↳ QDP
                                                                                                                                                                ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
                                                                                      ↳ QDP
                                                                                        ↳ RuleRemovalProof
                                                                                          ↳ QDP
                                                                                            ↳ RuleRemovalProof
                                                                                              ↳ QDP
                                                                                                ↳ RuleRemovalProof
                                                                                                  ↳ QDP
                                                                                                    ↳ RuleRemovalProof
                                                                                                      ↳ QDP
                                                                                                        ↳ RuleRemovalProof
                                                                                                          ↳ QDP
                                                                                                            ↳ RuleRemovalProof
                                                                                                              ↳ QDP
                                                                                                                ↳ RuleRemovalProof
                                                                                                                  ↳ QDP
                                                                                                                    ↳ RuleRemovalProof
                                                                                                                      ↳ QDP
                                                                                                                        ↳ RuleRemovalProof
                                                                                                                          ↳ QDP
                                                                                                                            ↳ RuleRemovalProof
                                                                                                                              ↳ QDP
                                                                                                                                ↳ RuleRemovalProof
                                                                                                                                  ↳ QDP
                                                                                                                                    ↳ RuleRemovalProof
                                                                                                                                      ↳ QDP
                                                                                                                                        ↳ RuleRemovalProof
                                                                                                                                          ↳ QDP
                                                                                                                                            ↳ RuleRemovalProof
                                                                                                                                              ↳ QDP
                                                                                                                                                ↳ RuleRemovalProof
                                                                                                                                                  ↳ QDP
                                                                                                                                                    ↳ RuleRemovalProof
                                                                                                                                                      ↳ QDP
                                                                                                                                                        ↳ RuleRemovalProof
                                                                                                                                                          ↳ QDP
                                                                                                                                                            ↳ RuleRemovalProof
                                                                                                                                                              ↳ QDP
                                                                                                                                                                ↳ RuleRemovalProof
                                                                                                                                                                  ↳ QDP
                                                                                                                                                                    ↳ RuleRemovalProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.


Used ordering: POLO with Polynomial interpretation:

POL(plus_22(x1, x2)) = x1 + x2   
POL(S2_2_IN_GA1(x1)) = 1 + x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ PiDPToQDPProof
                  ↳ QDP
                    ↳ QDPPoloProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ UsableRulesProof
                              ↳ QDP
                                ↳ RuleRemovalProof
                                  ↳ QDP
                                    ↳ RuleRemovalProof
                                      ↳ QDP
                                        ↳ RuleRemovalProof
                                          ↳ QDP
                                            ↳ RuleRemovalProof
                                              ↳ QDP
                                                ↳ RuleRemovalProof
                                                  ↳ QDP
                                                    ↳ RuleRemovalProof
                                                      ↳ QDP
                                                        ↳ RuleRemovalProof
                                                          ↳ QDP
                                                            ↳ RuleRemovalProof
                                                              ↳ QDP
                                                                ↳ QDPPoloProof
                                                                  ↳ QDP
                                                                    ↳ RuleRemovalProof
                                                                      ↳ QDP
                                                                        ↳ RuleRemovalProof
                                                                          ↳ QDP
                                                                            ↳ RuleRemovalProof
                                                                              ↳ QDP
                                                                                ↳ RuleRemovalProof
                                                                                  ↳ QDP
                                                                                    ↳ RuleRemovalProof
                                                                                      ↳ QDP
                                                                                        ↳ RuleRemovalProof
                                                                                          ↳ QDP
                                                                                            ↳ RuleRemovalProof
                                                                                              ↳ QDP
                                                                                                ↳ RuleRemovalProof
                                                                                                  ↳ QDP
                                                                                                    ↳ RuleRemovalProof
                                                                                                      ↳ QDP
                                                                                                        ↳ RuleRemovalProof
                                                                                                          ↳ QDP
                                                                                                            ↳ RuleRemovalProof
                                                                                                              ↳ QDP
                                                                                                                ↳ RuleRemovalProof
                                                                                                                  ↳ QDP
                                                                                                                    ↳ RuleRemovalProof
                                                                                                                      ↳ QDP
                                                                                                                        ↳ RuleRemovalProof
                                                                                                                          ↳ QDP
                                                                                                                            ↳ RuleRemovalProof
                                                                                                                              ↳ QDP
                                                                                                                                ↳ RuleRemovalProof
                                                                                                                                  ↳ QDP
                                                                                                                                    ↳ RuleRemovalProof
                                                                                                                                      ↳ QDP
                                                                                                                                        ↳ RuleRemovalProof
                                                                                                                                          ↳ QDP
                                                                                                                                            ↳ RuleRemovalProof
                                                                                                                                              ↳ QDP
                                                                                                                                                ↳ RuleRemovalProof
                                                                                                                                                  ↳ QDP
                                                                                                                                                    ↳ RuleRemovalProof
                                                                                                                                                      ↳ QDP
                                                                                                                                                        ↳ RuleRemovalProof
                                                                                                                                                          ↳ QDP
                                                                                                                                                            ↳ RuleRemovalProof
                                                                                                                                                              ↳ QDP
                                                                                                                                                                ↳ RuleRemovalProof
                                                                                                                                                                  ↳ QDP
                                                                                                                                                                    ↳ RuleRemovalProof
                                                                                                                                                                      ↳ QDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA1(plus_22(A, B)) -> S2_2_IN_GA1(plus_22(B, A))
S2_2_IN_GA1(plus_22(A, plus_22(B, C))) -> S2_2_IN_GA1(plus_22(plus_22(A, B), C))

R is empty.
The set Q consists of the following terms:

s2_2_in_ga1(x0)
isNat_1_in_g1(x0)
if_isNat_1_in_1_g1(x0)
if_s2_2_in_6_ga3(x0, x1, x2)
if_s2_2_in_7_ga3(x0, x1, x2)
add_3_in_gga2(x0, x1)
if_add_3_in_1_gga1(x0)
if_s2_2_in_8_ga1(x0)
if_s2_2_in_3_ga2(x0, x1)
if_s2_2_in_4_ga2(x0, x1)
if_s2_2_in_5_ga1(x0)
if_s2_2_in_2_ga1(x0)
if_s2_2_in_1_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2_2_IN_GA1}.
With regard to the inferred argument filtering the predicates were used in the following modes:
s22: (b,f)
isNat1: (b)
add3: (b,b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

s2_2_in_ga2(plus_22(A, plus_22(B, C)), D) -> if_s2_2_in_1_ga5(A, B, C, D, s2_2_in_ga2(plus_22(plus_22(A, B), C), D))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_2_ga4(A, B, C, s2_2_in_ga2(plus_22(B, A), C))
s2_2_in_ga2(plus_22(X, 0_0), X) -> s2_2_out_ga2(plus_22(X, 0_0), X)
s2_2_in_ga2(plus_22(X, Y), Z) -> if_s2_2_in_3_ga4(X, Y, Z, s2_2_in_ga2(X, A))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_6_ga4(A, B, C, isNat_1_in_g1(A))
isNat_1_in_g1(s_11(X)) -> if_isNat_1_in_1_g2(X, isNat_1_in_g1(X))
isNat_1_in_g1(0_0) -> isNat_1_out_g1(0_0)
if_isNat_1_in_1_g2(X, isNat_1_out_g1(X)) -> isNat_1_out_g1(s_11(X))
if_s2_2_in_6_ga4(A, B, C, isNat_1_out_g1(A)) -> if_s2_2_in_7_ga4(A, B, C, isNat_1_in_g1(B))
if_s2_2_in_7_ga4(A, B, C, isNat_1_out_g1(B)) -> if_s2_2_in_8_ga4(A, B, C, add_3_in_gga3(A, B, C))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_s2_2_in_8_ga4(A, B, C, add_3_out_gga3(A, B, C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_3_ga4(X, Y, Z, s2_2_out_ga2(X, A)) -> if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_in_ga2(Y, B))
if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_out_ga2(Y, B)) -> if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_in_ga2(plus_22(A, B), Z))
if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_out_ga2(plus_22(A, B), Z)) -> s2_2_out_ga2(plus_22(X, Y), Z)
if_s2_2_in_2_ga4(A, B, C, s2_2_out_ga2(plus_22(B, A), C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_1_ga5(A, B, C, D, s2_2_out_ga2(plus_22(plus_22(A, B), C), D)) -> s2_2_out_ga2(plus_22(A, plus_22(B, C)), D)

The argument filtering Pi contains the following mapping:
s2_2_in_ga2(x1, x2)  =  s2_2_in_ga1(x1)
plus_22(x1, x2)  =  plus_22(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
if_s2_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_1_ga4(x1, x2, x3, x5)
if_s2_2_in_2_ga4(x1, x2, x3, x4)  =  if_s2_2_in_2_ga3(x1, x2, x4)
s2_2_out_ga2(x1, x2)  =  s2_2_out_ga2(x1, x2)
if_s2_2_in_3_ga4(x1, x2, x3, x4)  =  if_s2_2_in_3_ga3(x1, x2, x4)
if_s2_2_in_6_ga4(x1, x2, x3, x4)  =  if_s2_2_in_6_ga3(x1, x2, x4)
isNat_1_in_g1(x1)  =  isNat_1_in_g1(x1)
if_isNat_1_in_1_g2(x1, x2)  =  if_isNat_1_in_1_g2(x1, x2)
isNat_1_out_g1(x1)  =  isNat_1_out_g1(x1)
if_s2_2_in_7_ga4(x1, x2, x3, x4)  =  if_s2_2_in_7_ga3(x1, x2, x4)
if_s2_2_in_8_ga4(x1, x2, x3, x4)  =  if_s2_2_in_8_ga3(x1, x2, x4)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga3(x1, x2, x4)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga3(x1, x2, x3)
if_s2_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_4_ga4(x1, x2, x4, x5)
if_s2_2_in_5_ga6(x1, x2, x3, x4, x5, x6)  =  if_s2_2_in_5_ga3(x1, x2, x6)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

s2_2_in_ga2(plus_22(A, plus_22(B, C)), D) -> if_s2_2_in_1_ga5(A, B, C, D, s2_2_in_ga2(plus_22(plus_22(A, B), C), D))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_2_ga4(A, B, C, s2_2_in_ga2(plus_22(B, A), C))
s2_2_in_ga2(plus_22(X, 0_0), X) -> s2_2_out_ga2(plus_22(X, 0_0), X)
s2_2_in_ga2(plus_22(X, Y), Z) -> if_s2_2_in_3_ga4(X, Y, Z, s2_2_in_ga2(X, A))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_6_ga4(A, B, C, isNat_1_in_g1(A))
isNat_1_in_g1(s_11(X)) -> if_isNat_1_in_1_g2(X, isNat_1_in_g1(X))
isNat_1_in_g1(0_0) -> isNat_1_out_g1(0_0)
if_isNat_1_in_1_g2(X, isNat_1_out_g1(X)) -> isNat_1_out_g1(s_11(X))
if_s2_2_in_6_ga4(A, B, C, isNat_1_out_g1(A)) -> if_s2_2_in_7_ga4(A, B, C, isNat_1_in_g1(B))
if_s2_2_in_7_ga4(A, B, C, isNat_1_out_g1(B)) -> if_s2_2_in_8_ga4(A, B, C, add_3_in_gga3(A, B, C))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_s2_2_in_8_ga4(A, B, C, add_3_out_gga3(A, B, C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_3_ga4(X, Y, Z, s2_2_out_ga2(X, A)) -> if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_in_ga2(Y, B))
if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_out_ga2(Y, B)) -> if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_in_ga2(plus_22(A, B), Z))
if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_out_ga2(plus_22(A, B), Z)) -> s2_2_out_ga2(plus_22(X, Y), Z)
if_s2_2_in_2_ga4(A, B, C, s2_2_out_ga2(plus_22(B, A), C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_1_ga5(A, B, C, D, s2_2_out_ga2(plus_22(plus_22(A, B), C), D)) -> s2_2_out_ga2(plus_22(A, plus_22(B, C)), D)

The argument filtering Pi contains the following mapping:
s2_2_in_ga2(x1, x2)  =  s2_2_in_ga1(x1)
plus_22(x1, x2)  =  plus_22(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
if_s2_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_1_ga4(x1, x2, x3, x5)
if_s2_2_in_2_ga4(x1, x2, x3, x4)  =  if_s2_2_in_2_ga3(x1, x2, x4)
s2_2_out_ga2(x1, x2)  =  s2_2_out_ga2(x1, x2)
if_s2_2_in_3_ga4(x1, x2, x3, x4)  =  if_s2_2_in_3_ga3(x1, x2, x4)
if_s2_2_in_6_ga4(x1, x2, x3, x4)  =  if_s2_2_in_6_ga3(x1, x2, x4)
isNat_1_in_g1(x1)  =  isNat_1_in_g1(x1)
if_isNat_1_in_1_g2(x1, x2)  =  if_isNat_1_in_1_g2(x1, x2)
isNat_1_out_g1(x1)  =  isNat_1_out_g1(x1)
if_s2_2_in_7_ga4(x1, x2, x3, x4)  =  if_s2_2_in_7_ga3(x1, x2, x4)
if_s2_2_in_8_ga4(x1, x2, x3, x4)  =  if_s2_2_in_8_ga3(x1, x2, x4)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga3(x1, x2, x4)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga3(x1, x2, x3)
if_s2_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_4_ga4(x1, x2, x4, x5)
if_s2_2_in_5_ga6(x1, x2, x3, x4, x5, x6)  =  if_s2_2_in_5_ga3(x1, x2, x6)


Pi DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA2(plus_22(A, plus_22(B, C)), D) -> IF_S2_2_IN_1_GA5(A, B, C, D, s2_2_in_ga2(plus_22(plus_22(A, B), C), D))
S2_2_IN_GA2(plus_22(A, plus_22(B, C)), D) -> S2_2_IN_GA2(plus_22(plus_22(A, B), C), D)
S2_2_IN_GA2(plus_22(A, B), C) -> IF_S2_2_IN_2_GA4(A, B, C, s2_2_in_ga2(plus_22(B, A), C))
S2_2_IN_GA2(plus_22(A, B), C) -> S2_2_IN_GA2(plus_22(B, A), C)
S2_2_IN_GA2(plus_22(X, Y), Z) -> IF_S2_2_IN_3_GA4(X, Y, Z, s2_2_in_ga2(X, A))
S2_2_IN_GA2(plus_22(X, Y), Z) -> S2_2_IN_GA2(X, A)
S2_2_IN_GA2(plus_22(A, B), C) -> IF_S2_2_IN_6_GA4(A, B, C, isNat_1_in_g1(A))
S2_2_IN_GA2(plus_22(A, B), C) -> ISNAT_1_IN_G1(A)
ISNAT_1_IN_G1(s_11(X)) -> IF_ISNAT_1_IN_1_G2(X, isNat_1_in_g1(X))
ISNAT_1_IN_G1(s_11(X)) -> ISNAT_1_IN_G1(X)
IF_S2_2_IN_6_GA4(A, B, C, isNat_1_out_g1(A)) -> IF_S2_2_IN_7_GA4(A, B, C, isNat_1_in_g1(B))
IF_S2_2_IN_6_GA4(A, B, C, isNat_1_out_g1(A)) -> ISNAT_1_IN_G1(B)
IF_S2_2_IN_7_GA4(A, B, C, isNat_1_out_g1(B)) -> IF_S2_2_IN_8_GA4(A, B, C, add_3_in_gga3(A, B, C))
IF_S2_2_IN_7_GA4(A, B, C, isNat_1_out_g1(B)) -> ADD_3_IN_GGA3(A, B, C)
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> IF_ADD_3_IN_1_GGA4(X, Y, Z, add_3_in_gga3(X, Y, Z))
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> ADD_3_IN_GGA3(X, Y, Z)
IF_S2_2_IN_3_GA4(X, Y, Z, s2_2_out_ga2(X, A)) -> IF_S2_2_IN_4_GA5(X, Y, Z, A, s2_2_in_ga2(Y, B))
IF_S2_2_IN_3_GA4(X, Y, Z, s2_2_out_ga2(X, A)) -> S2_2_IN_GA2(Y, B)
IF_S2_2_IN_4_GA5(X, Y, Z, A, s2_2_out_ga2(Y, B)) -> IF_S2_2_IN_5_GA6(X, Y, Z, A, B, s2_2_in_ga2(plus_22(A, B), Z))
IF_S2_2_IN_4_GA5(X, Y, Z, A, s2_2_out_ga2(Y, B)) -> S2_2_IN_GA2(plus_22(A, B), Z)

The TRS R consists of the following rules:

s2_2_in_ga2(plus_22(A, plus_22(B, C)), D) -> if_s2_2_in_1_ga5(A, B, C, D, s2_2_in_ga2(plus_22(plus_22(A, B), C), D))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_2_ga4(A, B, C, s2_2_in_ga2(plus_22(B, A), C))
s2_2_in_ga2(plus_22(X, 0_0), X) -> s2_2_out_ga2(plus_22(X, 0_0), X)
s2_2_in_ga2(plus_22(X, Y), Z) -> if_s2_2_in_3_ga4(X, Y, Z, s2_2_in_ga2(X, A))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_6_ga4(A, B, C, isNat_1_in_g1(A))
isNat_1_in_g1(s_11(X)) -> if_isNat_1_in_1_g2(X, isNat_1_in_g1(X))
isNat_1_in_g1(0_0) -> isNat_1_out_g1(0_0)
if_isNat_1_in_1_g2(X, isNat_1_out_g1(X)) -> isNat_1_out_g1(s_11(X))
if_s2_2_in_6_ga4(A, B, C, isNat_1_out_g1(A)) -> if_s2_2_in_7_ga4(A, B, C, isNat_1_in_g1(B))
if_s2_2_in_7_ga4(A, B, C, isNat_1_out_g1(B)) -> if_s2_2_in_8_ga4(A, B, C, add_3_in_gga3(A, B, C))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_s2_2_in_8_ga4(A, B, C, add_3_out_gga3(A, B, C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_3_ga4(X, Y, Z, s2_2_out_ga2(X, A)) -> if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_in_ga2(Y, B))
if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_out_ga2(Y, B)) -> if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_in_ga2(plus_22(A, B), Z))
if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_out_ga2(plus_22(A, B), Z)) -> s2_2_out_ga2(plus_22(X, Y), Z)
if_s2_2_in_2_ga4(A, B, C, s2_2_out_ga2(plus_22(B, A), C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_1_ga5(A, B, C, D, s2_2_out_ga2(plus_22(plus_22(A, B), C), D)) -> s2_2_out_ga2(plus_22(A, plus_22(B, C)), D)

The argument filtering Pi contains the following mapping:
s2_2_in_ga2(x1, x2)  =  s2_2_in_ga1(x1)
plus_22(x1, x2)  =  plus_22(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
if_s2_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_1_ga4(x1, x2, x3, x5)
if_s2_2_in_2_ga4(x1, x2, x3, x4)  =  if_s2_2_in_2_ga3(x1, x2, x4)
s2_2_out_ga2(x1, x2)  =  s2_2_out_ga2(x1, x2)
if_s2_2_in_3_ga4(x1, x2, x3, x4)  =  if_s2_2_in_3_ga3(x1, x2, x4)
if_s2_2_in_6_ga4(x1, x2, x3, x4)  =  if_s2_2_in_6_ga3(x1, x2, x4)
isNat_1_in_g1(x1)  =  isNat_1_in_g1(x1)
if_isNat_1_in_1_g2(x1, x2)  =  if_isNat_1_in_1_g2(x1, x2)
isNat_1_out_g1(x1)  =  isNat_1_out_g1(x1)
if_s2_2_in_7_ga4(x1, x2, x3, x4)  =  if_s2_2_in_7_ga3(x1, x2, x4)
if_s2_2_in_8_ga4(x1, x2, x3, x4)  =  if_s2_2_in_8_ga3(x1, x2, x4)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga3(x1, x2, x4)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga3(x1, x2, x3)
if_s2_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_4_ga4(x1, x2, x4, x5)
if_s2_2_in_5_ga6(x1, x2, x3, x4, x5, x6)  =  if_s2_2_in_5_ga3(x1, x2, x6)
IF_S2_2_IN_3_GA4(x1, x2, x3, x4)  =  IF_S2_2_IN_3_GA3(x1, x2, x4)
IF_S2_2_IN_6_GA4(x1, x2, x3, x4)  =  IF_S2_2_IN_6_GA3(x1, x2, x4)
ADD_3_IN_GGA3(x1, x2, x3)  =  ADD_3_IN_GGA2(x1, x2)
S2_2_IN_GA2(x1, x2)  =  S2_2_IN_GA1(x1)
IF_S2_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_S2_2_IN_1_GA4(x1, x2, x3, x5)
IF_S2_2_IN_8_GA4(x1, x2, x3, x4)  =  IF_S2_2_IN_8_GA3(x1, x2, x4)
IF_S2_2_IN_2_GA4(x1, x2, x3, x4)  =  IF_S2_2_IN_2_GA3(x1, x2, x4)
IF_S2_2_IN_5_GA6(x1, x2, x3, x4, x5, x6)  =  IF_S2_2_IN_5_GA3(x1, x2, x6)
IF_ADD_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_ADD_3_IN_1_GGA3(x1, x2, x4)
ISNAT_1_IN_G1(x1)  =  ISNAT_1_IN_G1(x1)
IF_ISNAT_1_IN_1_G2(x1, x2)  =  IF_ISNAT_1_IN_1_G2(x1, x2)
IF_S2_2_IN_7_GA4(x1, x2, x3, x4)  =  IF_S2_2_IN_7_GA3(x1, x2, x4)
IF_S2_2_IN_4_GA5(x1, x2, x3, x4, x5)  =  IF_S2_2_IN_4_GA4(x1, x2, x4, x5)

We have to consider all (P,R,Pi)-chains

↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

S2_2_IN_GA2(plus_22(A, plus_22(B, C)), D) -> IF_S2_2_IN_1_GA5(A, B, C, D, s2_2_in_ga2(plus_22(plus_22(A, B), C), D))
S2_2_IN_GA2(plus_22(A, plus_22(B, C)), D) -> S2_2_IN_GA2(plus_22(plus_22(A, B), C), D)
S2_2_IN_GA2(plus_22(A, B), C) -> IF_S2_2_IN_2_GA4(A, B, C, s2_2_in_ga2(plus_22(B, A), C))
S2_2_IN_GA2(plus_22(A, B), C) -> S2_2_IN_GA2(plus_22(B, A), C)
S2_2_IN_GA2(plus_22(X, Y), Z) -> IF_S2_2_IN_3_GA4(X, Y, Z, s2_2_in_ga2(X, A))
S2_2_IN_GA2(plus_22(X, Y), Z) -> S2_2_IN_GA2(X, A)
S2_2_IN_GA2(plus_22(A, B), C) -> IF_S2_2_IN_6_GA4(A, B, C, isNat_1_in_g1(A))
S2_2_IN_GA2(plus_22(A, B), C) -> ISNAT_1_IN_G1(A)
ISNAT_1_IN_G1(s_11(X)) -> IF_ISNAT_1_IN_1_G2(X, isNat_1_in_g1(X))
ISNAT_1_IN_G1(s_11(X)) -> ISNAT_1_IN_G1(X)
IF_S2_2_IN_6_GA4(A, B, C, isNat_1_out_g1(A)) -> IF_S2_2_IN_7_GA4(A, B, C, isNat_1_in_g1(B))
IF_S2_2_IN_6_GA4(A, B, C, isNat_1_out_g1(A)) -> ISNAT_1_IN_G1(B)
IF_S2_2_IN_7_GA4(A, B, C, isNat_1_out_g1(B)) -> IF_S2_2_IN_8_GA4(A, B, C, add_3_in_gga3(A, B, C))
IF_S2_2_IN_7_GA4(A, B, C, isNat_1_out_g1(B)) -> ADD_3_IN_GGA3(A, B, C)
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> IF_ADD_3_IN_1_GGA4(X, Y, Z, add_3_in_gga3(X, Y, Z))
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> ADD_3_IN_GGA3(X, Y, Z)
IF_S2_2_IN_3_GA4(X, Y, Z, s2_2_out_ga2(X, A)) -> IF_S2_2_IN_4_GA5(X, Y, Z, A, s2_2_in_ga2(Y, B))
IF_S2_2_IN_3_GA4(X, Y, Z, s2_2_out_ga2(X, A)) -> S2_2_IN_GA2(Y, B)
IF_S2_2_IN_4_GA5(X, Y, Z, A, s2_2_out_ga2(Y, B)) -> IF_S2_2_IN_5_GA6(X, Y, Z, A, B, s2_2_in_ga2(plus_22(A, B), Z))
IF_S2_2_IN_4_GA5(X, Y, Z, A, s2_2_out_ga2(Y, B)) -> S2_2_IN_GA2(plus_22(A, B), Z)

The TRS R consists of the following rules:

s2_2_in_ga2(plus_22(A, plus_22(B, C)), D) -> if_s2_2_in_1_ga5(A, B, C, D, s2_2_in_ga2(plus_22(plus_22(A, B), C), D))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_2_ga4(A, B, C, s2_2_in_ga2(plus_22(B, A), C))
s2_2_in_ga2(plus_22(X, 0_0), X) -> s2_2_out_ga2(plus_22(X, 0_0), X)
s2_2_in_ga2(plus_22(X, Y), Z) -> if_s2_2_in_3_ga4(X, Y, Z, s2_2_in_ga2(X, A))
s2_2_in_ga2(plus_22(A, B), C) -> if_s2_2_in_6_ga4(A, B, C, isNat_1_in_g1(A))
isNat_1_in_g1(s_11(X)) -> if_isNat_1_in_1_g2(X, isNat_1_in_g1(X))
isNat_1_in_g1(0_0) -> isNat_1_out_g1(0_0)
if_isNat_1_in_1_g2(X, isNat_1_out_g1(X)) -> isNat_1_out_g1(s_11(X))
if_s2_2_in_6_ga4(A, B, C, isNat_1_out_g1(A)) -> if_s2_2_in_7_ga4(A, B, C, isNat_1_in_g1(B))
if_s2_2_in_7_ga4(A, B, C, isNat_1_out_g1(B)) -> if_s2_2_in_8_ga4(A, B, C, add_3_in_gga3(A, B, C))
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_s2_2_in_8_ga4(A, B, C, add_3_out_gga3(A, B, C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_3_ga4(X, Y, Z, s2_2_out_ga2(X, A)) -> if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_in_ga2(Y, B))
if_s2_2_in_4_ga5(X, Y, Z, A, s2_2_out_ga2(Y, B)) -> if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_in_ga2(plus_22(A, B), Z))
if_s2_2_in_5_ga6(X, Y, Z, A, B, s2_2_out_ga2(plus_22(A, B), Z)) -> s2_2_out_ga2(plus_22(X, Y), Z)
if_s2_2_in_2_ga4(A, B, C, s2_2_out_ga2(plus_22(B, A), C)) -> s2_2_out_ga2(plus_22(A, B), C)
if_s2_2_in_1_ga5(A, B, C, D, s2_2_out_ga2(plus_22(plus_22(A, B), C), D)) -> s2_2_out_ga2(plus_22(A, plus_22(B, C)), D)

The argument filtering Pi contains the following mapping:
s2_2_in_ga2(x1, x2)  =  s2_2_in_ga1(x1)
plus_22(x1, x2)  =  plus_22(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
if_s2_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_1_ga4(x1, x2, x3, x5)
if_s2_2_in_2_ga4(x1, x2, x3, x4)  =  if_s2_2_in_2_ga3(x1, x2, x4)
s2_2_out_ga2(x1, x2)  =  s2_2_out_ga2(x1, x2)
if_s2_2_in_3_ga4(x1, x2, x3, x4)  =  if_s2_2_in_3_ga3(x1, x2, x4)
if_s2_2_in_6_ga4(x1, x2, x3, x4)  =  if_s2_2_in_6_ga3(x1, x2, x4)
isNat_1_in_g1(x1)  =  isNat_1_in_g1(x1)
if_isNat_1_in_1_g2(x1, x2)  =  if_isNat_1_in_1_g2(x1, x2)
isNat_1_out_g1(x1)  =  isNat_1_out_g1(x1)
if_s2_2_in_7_ga4(x1, x2, x3, x4)  =  if_s2_2_in_7_ga3(x1, x2, x4)
if_s2_2_in_8_ga4(x1, x2, x3, x4)  =  if_s2_2_in_8_ga3(x1, x2, x4)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga3(x1, x2, x4)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga3(x1, x2, x3)
if_s2_2_in_4_ga5(x1, x2, x3, x4, x5)  =  if_s2_2_in_4_ga4(x1, x2, x4, x5)
if_s2_2_in_5_ga6(x1, x2, x3, x4, x5, x6)  =  if_s2_2_in_5_ga3(x1, x2, x6)
IF_S2_2_IN_3_GA4(x1, x2, x3, x4)  =  IF_S2_2_IN_3_GA3(x1, x2, x4)
IF_S2_2_IN_6_GA4(x1, x2, x3, x4)  =  IF_S2_2_IN_6_GA3(x1, x2, x4)
ADD_3_IN_GGA3(x1, x2, x3)  =  ADD_3_IN_GGA2(x1, x2)
S2_2_IN_GA2(x1, x2)  =  S2_2_IN_GA1(x1)
IF_S2_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_S2_2_IN_1_GA4(x1, x2, x3, x5)
IF_S2_2_IN_8_GA4(x1, x2, x3, x4)  =  IF_S2_2_IN_8_GA3(x1, x2, x4)
IF_S2_2_IN_2_GA4(x1, x2, x3, x4)  =  IF_S2_2_IN_2_GA3(x1, x2, x4)
IF_S2_2_IN_5_GA6(x1, x2, x3, x4, x5, x6)  =  IF_S2_2_IN_5_GA3(x1, x2, x6)
IF_ADD_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_ADD_3_IN_1_GGA3(x1, x2, x4)
ISNAT_1_IN_G1(x1)  =  ISNAT_1_IN_G1(x1)
IF_ISNAT_1_IN_1_G2(x1, x2)  =  IF_ISNAT_1_IN_1_G2(x1, x2)
IF_S2_2_IN_7_GA4(x1, x2, x3, x4)  =  IF_S2_2_IN_7_GA3(x1, x2, x4)
IF_S2_2_IN_4_GA5(x1, x2, x3, x4, x5)  =  IF_S2_2_IN_4_GA4(x1, x2, x4, x5)

We have to consider all (P,R,Pi)-chains